|
In program analysis, a shape analysis is a static code analysis technique that discovers and verifies properties of linked, dynamically allocated data structures in (usually imperative) computer programs. It is typically used at compile time to find software bugs or to verify high-level correctness properties of programs. In Java programs, it can be used to ensure that a sort method correctly sorts a list. For C programs, it might look for places where a block of memory is not properly freed. ==Applications== Shape analysis has been applied to a variety of problems: * Memory safety: finding memory leaks, dereferences of dangling pointers, and discovering cases where a block of memory is freed more than once.〔Rinetzky, Noam, and Mooly Sagiv. "Interprocedural shape analysis for recursive programs." Compiler Construction. Springer Berlin Heidelberg, 2001.〕〔Berdine, Josh, et al. "Shape analysis for composite data structures." Computer Aided Verification. Springer Berlin Heidelberg, 2007.〕 * Finding array out-of-bounds errors * Checking type-state properties (for example, ensuring that a file is open() before it is read()) * Ensuring that a method to reverse a linked list does not introduce cycles into the list〔 * Verifying that a sort method returns a result that is in sorted order 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Shape analysis (program analysis)」の詳細全文を読む スポンサード リンク
|